Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | // Automatically generated by cegarmc |
2 | // |
3 | |
4 | extern void __VERIFIER_assume(int); |
5 | extern int __VERIFIER_nondet_bool(); |
6 | extern char __VERIFIER_nondet_char(); |
7 | extern signed char __VERIFIER_nondet_schar(); |
8 | extern unsigned char __VERIFIER_nondet_uchar(); |
9 | extern int __VERIFIER_nondet_int(); |
10 | extern unsigned int __VERIFIER_nondet_uint(); |
11 | extern short __VERIFIER_nondet_short(); |
12 | extern unsigned short __VERIFIER_nondet_ushort(); |
13 | extern long __VERIFIER_nondet_long(); |
14 | extern unsigned long __VERIFIER_nondet_ulong(); |
15 | extern long long __VERIFIER_nondet_longlong(); |
16 | extern unsigned long long __VERIFIER_nondet_ull(); |
17 | extern float __VERIFIER_nondet_float(); |
18 | extern double __VERIFIER_nondet_double(); |
19 | extern long double __VERIFIER_nondet_longdouble(); |
20 | extern void * __VERIFIER_nondet_pointer(); |
21 | |
22 | int D_print_i; |
23 | int D_print_st; |
24 | int D_z; |
25 | int N_generate_i; |
26 | int N_generate_st; |
27 | int S1_addsub_i; |
28 | int S1_addsub_st; |
29 | int S2_presdbl_i; |
30 | int S2_presdbl_st; |
31 | int S3_zero_i; |
32 | int S3_zero_st; |
33 | int count; |
34 | int main_clk_ev; |
35 | int main_clk_neg_edge; |
36 | int main_clk_pos_edge; |
37 | int main_clk_req_up; |
38 | int main_clk_val; |
39 | int main_clk_val_t; |
40 | int main_dbl_ev; |
41 | int main_dbl_req_up; |
42 | int main_dbl_val; |
43 | int main_dbl_val_t; |
44 | int main_diff_ev; |
45 | int main_diff_req_up; |
46 | int main_diff_val; |
47 | int main_diff_val_t; |
48 | int main_in1_ev; |
49 | int main_in1_req_up; |
50 | int main_in1_val; |
51 | int main_in1_val_t; |
52 | int main_in2_ev; |
53 | int main_in2_req_up; |
54 | int main_in2_val; |
55 | int main_in2_val_t; |
56 | int main_pres_ev; |
57 | int main_pres_req_up; |
58 | int main_pres_val; |
59 | int main_pres_val_t; |
60 | int main_sum_ev; |
61 | int main_sum_req_up; |
62 | int main_sum_val; |
63 | int main_sum_val_t; |
64 | int main_zero_ev; |
65 | int main_zero_req_up; |
66 | int main_zero_val; |
67 | int main_zero_val_t; |
68 | int res; |
69 | |
70 | void error(); |
71 | void N_generate(); |
72 | void S1_addsub(); |
73 | void S2_presdbl(); |
74 | void S3_zero(); |
75 | void D_print(); |
76 | void eval(); |
77 | void start_simulation(); |
78 | |
79 | |
80 | void error() { |
81 | { |
82 | goto ERROR; |
83 | ERROR: ; |
84 | return; |
85 | } |
86 | } |
87 | |
88 | void N_generate() { |
89 | auto int a; |
90 | auto int b; |
91 | { |
92 | main_in1_val_t = __VERIFIER_nondet_int(); |
93 | main_in1_req_up = 1; |
94 | main_in2_val_t = __VERIFIER_nondet_int(); |
95 | main_in2_req_up = 1; |
96 | return; |
97 | } |
98 | } |
99 | |
100 | void S1_addsub() { |
101 | auto int a; |
102 | auto int b; |
103 | { |
104 | a = main_in1_val; |
105 | b = main_in2_val; |
106 | main_sum_val_t = a + b; |
107 | main_sum_req_up = 1; |
108 | main_diff_val_t = a - b; |
109 | main_diff_req_up = 1; |
110 | return; |
111 | } |
112 | } |
113 | |
114 | void S2_presdbl() { |
115 | auto int a; |
116 | auto int b; |
117 | auto int c; |
118 | auto int d; |
119 | { |
120 | a = main_sum_val; |
121 | b = main_diff_val; |
122 | main_pres_val_t = a; |
123 | main_pres_req_up = 1; |
124 | c = a + b; |
125 | d = a - b; |
126 | main_dbl_val_t = c + d; |
127 | main_dbl_req_up = 1; |
128 | return; |
129 | } |
130 | } |
131 | |
132 | void S3_zero() { |
133 | auto int a; |
134 | auto int b; |
135 | { |
136 | a = main_pres_val; |
137 | b = main_dbl_val; |
138 | main_zero_val_t = b - (a + a); |
139 | main_zero_req_up = 1; |
140 | return; |
141 | } |
142 | } |
143 | |
144 | void D_print() { |
145 | { |
146 | D_z = main_zero_val; |
147 | return; |
148 | } |
149 | } |
150 | |
151 | void eval() { |
152 | auto int tmp; |
153 | auto int tmp___0; |
154 | auto int tmp___1; |
155 | auto int tmp___2; |
156 | auto int tmp___3; |
157 | { |
158 | { |
159 | while (1) { |
160 | { |
161 | while_0_continue: ; |
162 | if (N_generate_st == 0) { |
163 | } |
164 | else { |
165 | if (S1_addsub_st == 0) { |
166 | } |
167 | else { |
168 | if (S2_presdbl_st == 0) { |
169 | } |
170 | else { |
171 | if (S3_zero_st == 0) { |
172 | } |
173 | else { |
174 | if (D_print_st == 0) { |
175 | } |
176 | else { |
177 | goto while_0_break; |
178 | } |
179 | } |
180 | } |
181 | } |
182 | } |
183 | if (N_generate_st == 0) { |
184 | { |
185 | tmp = __VERIFIER_nondet_int(); |
186 | } |
187 | if (tmp) { |
188 | N_generate_st = 1; |
189 | N_generate(); |
190 | } |
191 | else { |
192 | } |
193 | } |
194 | else { |
195 | } |
196 | if (S1_addsub_st == 0) { |
197 | { |
198 | tmp___0 = __VERIFIER_nondet_int(); |
199 | } |
200 | if (tmp___0) { |
201 | S1_addsub_st = 1; |
202 | S1_addsub(); |
203 | } |
204 | else { |
205 | } |
206 | } |
207 | else { |
208 | } |
209 | if (S2_presdbl_st == 0) { |
210 | { |
211 | tmp___1 = __VERIFIER_nondet_int(); |
212 | } |
213 | if (tmp___1) { |
214 | S2_presdbl_st = 1; |
215 | S2_presdbl(); |
216 | } |
217 | else { |
218 | } |
219 | } |
220 | else { |
221 | } |
222 | if (S3_zero_st == 0) { |
223 | { |
224 | tmp___2 = __VERIFIER_nondet_int(); |
225 | } |
226 | if (tmp___2) { |
227 | S3_zero_st = 1; |
228 | S3_zero(); |
229 | } |
230 | else { |
231 | } |
232 | } |
233 | else { |
234 | } |
235 | if (D_print_st == 0) { |
236 | { |
237 | tmp___3 = __VERIFIER_nondet_int(); |
238 | } |
239 | if (tmp___3) { |
240 | D_print_st = 1; |
241 | D_print(); |
242 | } |
243 | else { |
244 | } |
245 | } |
246 | else { |
247 | } |
248 | } |
249 | } |
250 | while_0_break: ; |
251 | } |
252 | return; |
253 | } |
254 | } |
255 | |
256 | void start_simulation() { |
257 | auto int kernel_st; |
258 | { |
259 | kernel_st = 0; |
260 | if (main_in1_req_up == 1) { |
261 | if (main_in1_val != main_in1_val_t) { |
262 | main_in1_val = main_in1_val_t; |
263 | main_in1_ev = 0; |
264 | } |
265 | else { |
266 | } |
267 | main_in1_req_up = 0; |
268 | } |
269 | else { |
270 | } |
271 | if (main_in2_req_up == 1) { |
272 | if (main_in2_val != main_in2_val_t) { |
273 | main_in2_val = main_in2_val_t; |
274 | main_in2_ev = 0; |
275 | } |
276 | else { |
277 | } |
278 | main_in2_req_up = 0; |
279 | } |
280 | else { |
281 | } |
282 | if (main_sum_req_up == 1) { |
283 | if (main_sum_val != main_sum_val_t) { |
284 | main_sum_val = main_sum_val_t; |
285 | main_sum_ev = 0; |
286 | } |
287 | else { |
288 | } |
289 | main_sum_req_up = 0; |
290 | } |
291 | else { |
292 | } |
293 | if (main_diff_req_up == 1) { |
294 | if (main_diff_val != main_diff_val_t) { |
295 | main_diff_val = main_diff_val_t; |
296 | main_diff_ev = 0; |
297 | } |
298 | else { |
299 | } |
300 | main_diff_req_up = 0; |
301 | } |
302 | else { |
303 | } |
304 | if (main_pres_req_up == 1) { |
305 | if (main_pres_val != main_pres_val_t) { |
306 | main_pres_val = main_pres_val_t; |
307 | main_pres_ev = 0; |
308 | } |
309 | else { |
310 | } |
311 | main_pres_req_up = 0; |
312 | } |
313 | else { |
314 | } |
315 | if (main_dbl_req_up == 1) { |
316 | if (main_dbl_val != main_dbl_val_t) { |
317 | main_dbl_val = main_dbl_val_t; |
318 | main_dbl_ev = 0; |
319 | } |
320 | else { |
321 | } |
322 | main_dbl_req_up = 0; |
323 | } |
324 | else { |
325 | } |
326 | if (main_zero_req_up == 1) { |
327 | if (main_zero_val != main_zero_val_t) { |
328 | main_zero_val = main_zero_val_t; |
329 | main_zero_ev = 0; |
330 | } |
331 | else { |
332 | } |
333 | main_zero_req_up = 0; |
334 | } |
335 | else { |
336 | } |
337 | if (main_clk_req_up == 1) { |
338 | if (main_clk_val != main_clk_val_t) { |
339 | main_clk_val = main_clk_val_t; |
340 | main_clk_ev = 0; |
341 | if (main_clk_val == 1) { |
342 | main_clk_pos_edge = 0; |
343 | main_clk_neg_edge = 2; |
344 | } |
345 | else { |
346 | main_clk_neg_edge = 0; |
347 | main_clk_pos_edge = 2; |
348 | } |
349 | } |
350 | else { |
351 | } |
352 | main_clk_req_up = 0; |
353 | } |
354 | else { |
355 | } |
356 | if (N_generate_i == 1) { |
357 | N_generate_st = 0; |
358 | } |
359 | else { |
360 | N_generate_st = 2; |
361 | } |
362 | if (S1_addsub_i == 1) { |
363 | S1_addsub_st = 0; |
364 | } |
365 | else { |
366 | S1_addsub_st = 2; |
367 | } |
368 | if (S2_presdbl_i == 1) { |
369 | S2_presdbl_st = 0; |
370 | } |
371 | else { |
372 | S2_presdbl_st = 2; |
373 | } |
374 | if (S3_zero_i == 1) { |
375 | S3_zero_st = 0; |
376 | } |
377 | else { |
378 | S3_zero_st = 2; |
379 | } |
380 | if (D_print_i == 1) { |
381 | D_print_st = 0; |
382 | } |
383 | else { |
384 | D_print_st = 2; |
385 | } |
386 | if (main_in1_ev == 0) { |
387 | main_in1_ev = 1; |
388 | } |
389 | else { |
390 | } |
391 | if (main_in2_ev == 0) { |
392 | main_in2_ev = 1; |
393 | } |
394 | else { |
395 | } |
396 | if (main_sum_ev == 0) { |
397 | main_sum_ev = 1; |
398 | } |
399 | else { |
400 | } |
401 | if (main_diff_ev == 0) { |
402 | main_diff_ev = 1; |
403 | } |
404 | else { |
405 | } |
406 | if (main_pres_ev == 0) { |
407 | main_pres_ev = 1; |
408 | } |
409 | else { |
410 | } |
411 | if (main_dbl_ev == 0) { |
412 | main_dbl_ev = 1; |
413 | } |
414 | else { |
415 | } |
416 | if (main_zero_ev == 0) { |
417 | main_zero_ev = 1; |
418 | } |
419 | else { |
420 | } |
421 | if (main_clk_ev == 0) { |
422 | main_clk_ev = 1; |
423 | } |
424 | else { |
425 | } |
426 | if (main_clk_pos_edge == 0) { |
427 | main_clk_pos_edge = 1; |
428 | } |
429 | else { |
430 | } |
431 | if (main_clk_neg_edge == 0) { |
432 | main_clk_neg_edge = 1; |
433 | } |
434 | else { |
435 | } |
436 | if (main_clk_pos_edge == 1) { |
437 | N_generate_st = 0; |
438 | } |
439 | else { |
440 | } |
441 | if (main_clk_pos_edge == 1) { |
442 | S1_addsub_st = 0; |
443 | } |
444 | else { |
445 | } |
446 | if (main_clk_pos_edge == 1) { |
447 | S2_presdbl_st = 0; |
448 | } |
449 | else { |
450 | } |
451 | if (main_clk_pos_edge == 1) { |
452 | S3_zero_st = 0; |
453 | } |
454 | else { |
455 | } |
456 | if (main_clk_pos_edge == 1) { |
457 | D_print_st = 0; |
458 | } |
459 | else { |
460 | } |
461 | if (main_in1_ev == 1) { |
462 | main_in1_ev = 2; |
463 | } |
464 | else { |
465 | } |
466 | if (main_in2_ev == 1) { |
467 | main_in2_ev = 2; |
468 | } |
469 | else { |
470 | } |
471 | if (main_sum_ev == 1) { |
472 | main_sum_ev = 2; |
473 | } |
474 | else { |
475 | } |
476 | if (main_diff_ev == 1) { |
477 | main_diff_ev = 2; |
478 | } |
479 | else { |
480 | } |
481 | if (main_pres_ev == 1) { |
482 | main_pres_ev = 2; |
483 | } |
484 | else { |
485 | } |
486 | if (main_dbl_ev == 1) { |
487 | main_dbl_ev = 2; |
488 | } |
489 | else { |
490 | } |
491 | if (main_zero_ev == 1) { |
492 | main_zero_ev = 2; |
493 | } |
494 | else { |
495 | } |
496 | if (main_clk_ev == 1) { |
497 | main_clk_ev = 2; |
498 | } |
499 | else { |
500 | } |
501 | if (main_clk_pos_edge == 1) { |
502 | main_clk_pos_edge = 2; |
503 | } |
504 | else { |
505 | } |
506 | if (main_clk_neg_edge == 1) { |
507 | main_clk_neg_edge = 2; |
508 | } |
509 | else { |
510 | } |
511 | { |
512 | while (1) { |
513 | { |
514 | while_1_continue: ; |
515 | { |
516 | kernel_st = 1; |
517 | eval(); |
518 | } |
519 | kernel_st = 2; |
520 | if (main_in1_req_up == 1) { |
521 | if (main_in1_val != main_in1_val_t) { |
522 | main_in1_val = main_in1_val_t; |
523 | main_in1_ev = 0; |
524 | } |
525 | else { |
526 | } |
527 | main_in1_req_up = 0; |
528 | } |
529 | else { |
530 | } |
531 | if (main_in2_req_up == 1) { |
532 | if (main_in2_val != main_in2_val_t) { |
533 | main_in2_val = main_in2_val_t; |
534 | main_in2_ev = 0; |
535 | } |
536 | else { |
537 | } |
538 | main_in2_req_up = 0; |
539 | } |
540 | else { |
541 | } |
542 | if (main_sum_req_up == 1) { |
543 | if (main_sum_val != main_sum_val_t) { |
544 | main_sum_val = main_sum_val_t; |
545 | main_sum_ev = 0; |
546 | } |
547 | else { |
548 | } |
549 | main_sum_req_up = 0; |
550 | } |
551 | else { |
552 | } |
553 | if (main_diff_req_up == 1) { |
554 | if (main_diff_val != main_diff_val_t) { |
555 | main_diff_val = main_diff_val_t; |
556 | main_diff_ev = 0; |
557 | } |
558 | else { |
559 | } |
560 | main_diff_req_up = 0; |
561 | } |
562 | else { |
563 | } |
564 | if (main_pres_req_up == 1) { |
565 | if (main_pres_val != main_pres_val_t) { |
566 | main_pres_val = main_pres_val_t; |
567 | main_pres_ev = 0; |
568 | } |
569 | else { |
570 | } |
571 | main_pres_req_up = 0; |
572 | } |
573 | else { |
574 | } |
575 | if (main_dbl_req_up == 1) { |
576 | if (main_dbl_val != main_dbl_val_t) { |
577 | main_dbl_val = main_dbl_val_t; |
578 | main_dbl_ev = 0; |
579 | } |
580 | else { |
581 | } |
582 | main_dbl_req_up = 0; |
583 | } |
584 | else { |
585 | } |
586 | if (main_zero_req_up == 1) { |
587 | if (main_zero_val != main_zero_val_t) { |
588 | main_zero_val = main_zero_val_t; |
589 | main_zero_ev = 0; |
590 | } |
591 | else { |
592 | } |
593 | main_zero_req_up = 0; |
594 | } |
595 | else { |
596 | } |
597 | if (main_clk_req_up == 1) { |
598 | if (main_clk_val != main_clk_val_t) { |
599 | main_clk_val = main_clk_val_t; |
600 | main_clk_ev = 0; |
601 | if (main_clk_val == 1) { |
602 | main_clk_pos_edge = 0; |
603 | main_clk_neg_edge = 2; |
604 | } |
605 | else { |
606 | main_clk_neg_edge = 0; |
607 | main_clk_pos_edge = 2; |
608 | } |
609 | } |
610 | else { |
611 | } |
612 | main_clk_req_up = 0; |
613 | } |
614 | else { |
615 | } |
616 | kernel_st = 3; |
617 | if (main_in1_ev == 0) { |
618 | main_in1_ev = 1; |
619 | } |
620 | else { |
621 | } |
622 | if (main_in2_ev == 0) { |
623 | main_in2_ev = 1; |
624 | } |
625 | else { |
626 | } |
627 | if (main_sum_ev == 0) { |
628 | main_sum_ev = 1; |
629 | } |
630 | else { |
631 | } |
632 | if (main_diff_ev == 0) { |
633 | main_diff_ev = 1; |
634 | } |
635 | else { |
636 | } |
637 | if (main_pres_ev == 0) { |
638 | main_pres_ev = 1; |
639 | } |
640 | else { |
641 | } |
642 | if (main_dbl_ev == 0) { |
643 | main_dbl_ev = 1; |
644 | } |
645 | else { |
646 | } |
647 | if (main_zero_ev == 0) { |
648 | main_zero_ev = 1; |
649 | } |
650 | else { |
651 | } |
652 | if (main_clk_ev == 0) { |
653 | main_clk_ev = 1; |
654 | } |
655 | else { |
656 | } |
657 | if (main_clk_pos_edge == 0) { |
658 | main_clk_pos_edge = 1; |
659 | } |
660 | else { |
661 | } |
662 | if (main_clk_neg_edge == 0) { |
663 | main_clk_neg_edge = 1; |
664 | } |
665 | else { |
666 | } |
667 | if (main_clk_pos_edge == 1) { |
668 | N_generate_st = 0; |
669 | } |
670 | else { |
671 | } |
672 | if (main_clk_pos_edge == 1) { |
673 | S1_addsub_st = 0; |
674 | } |
675 | else { |
676 | } |
677 | if (main_clk_pos_edge == 1) { |
678 | S2_presdbl_st = 0; |
679 | } |
680 | else { |
681 | } |
682 | if (main_clk_pos_edge == 1) { |
683 | S3_zero_st = 0; |
684 | } |
685 | else { |
686 | } |
687 | if (main_clk_pos_edge == 1) { |
688 | D_print_st = 0; |
689 | } |
690 | else { |
691 | } |
692 | if (main_in1_ev == 1) { |
693 | main_in1_ev = 2; |
694 | } |
695 | else { |
696 | } |
697 | if (main_in2_ev == 1) { |
698 | main_in2_ev = 2; |
699 | } |
700 | else { |
701 | } |
702 | if (main_sum_ev == 1) { |
703 | main_sum_ev = 2; |
704 | } |
705 | else { |
706 | } |
707 | if (main_diff_ev == 1) { |
708 | main_diff_ev = 2; |
709 | } |
710 | else { |
711 | } |
712 | if (main_pres_ev == 1) { |
713 | main_pres_ev = 2; |
714 | } |
715 | else { |
716 | } |
717 | if (main_dbl_ev == 1) { |
718 | main_dbl_ev = 2; |
719 | } |
720 | else { |
721 | } |
722 | if (main_zero_ev == 1) { |
723 | main_zero_ev = 2; |
724 | } |
725 | else { |
726 | } |
727 | if (main_clk_ev == 1) { |
728 | main_clk_ev = 2; |
729 | } |
730 | else { |
731 | } |
732 | if (main_clk_pos_edge == 1) { |
733 | main_clk_pos_edge = 2; |
734 | } |
735 | else { |
736 | } |
737 | if (main_clk_neg_edge == 1) { |
738 | main_clk_neg_edge = 2; |
739 | } |
740 | else { |
741 | } |
742 | if (N_generate_st == 0) { |
743 | } |
744 | else { |
745 | if (S1_addsub_st == 0) { |
746 | } |
747 | else { |
748 | if (S2_presdbl_st == 0) { |
749 | } |
750 | else { |
751 | if (S3_zero_st == 0) { |
752 | } |
753 | else { |
754 | if (D_print_st == 0) { |
755 | } |
756 | else { |
757 | goto while_1_break; |
758 | } |
759 | } |
760 | } |
761 | } |
762 | } |
763 | } |
764 | } |
765 | while_1_break: ; |
766 | } |
767 | return; |
768 | } |
769 | } |
770 | |
771 | void main () { |
772 | // |
773 | // Number of lvals: 62 |
774 | // Frama_C_interval: int (int min, int max) |
775 | // int (int min, int max) |
776 | // error: void (void) |
777 | // void (void) |
778 | // count: int |
779 | // int |
780 | // res: int |
781 | // int |
782 | // main_in1_val: int |
783 | // int |
784 | // main_in1_val_t: int |
785 | // int |
786 | // main_in1_ev: int |
787 | // int |
788 | // main_in1_req_up: int |
789 | // int |
790 | // main_in2_val: int |
791 | // int |
792 | // main_in2_val_t: int |
793 | // int |
794 | // main_in2_ev: int |
795 | // int |
796 | // main_in2_req_up: int |
797 | // int |
798 | // main_diff_val: int |
799 | // int |
800 | // main_diff_val_t: int |
801 | // int |
802 | // main_diff_ev: int |
803 | // int |
804 | // main_diff_req_up: int |
805 | // int |
806 | // main_sum_val: int |
807 | // int |
808 | // main_sum_val_t: int |
809 | // int |
810 | // main_sum_ev: int |
811 | // int |
812 | // main_sum_req_up: int |
813 | // int |
814 | // main_pres_val: int |
815 | // int |
816 | // main_pres_val_t: int |
817 | // int |
818 | // main_pres_ev: int |
819 | // int |
820 | // main_pres_req_up: int |
821 | // int |
822 | // main_dbl_val: int |
823 | // int |
824 | // main_dbl_val_t: int |
825 | // int |
826 | // main_dbl_ev: int |
827 | // int |
828 | // main_dbl_req_up: int |
829 | // int |
830 | // main_zero_val: int |
831 | // int |
832 | // main_zero_val_t: int |
833 | // int |
834 | // main_zero_ev: int |
835 | // int |
836 | // main_zero_req_up: int |
837 | // int |
838 | // main_clk_val: int |
839 | // int |
840 | // main_clk_val_t: int |
841 | // int |
842 | // main_clk_ev: int |
843 | // int |
844 | // main_clk_req_up: int |
845 | // int |
846 | // main_clk_pos_edge: int |
847 | // int |
848 | // main_clk_neg_edge: int |
849 | // int |
850 | // N_generate_st: int |
851 | // int |
852 | // N_generate_i: int |
853 | // int |
854 | // S1_addsub_st: int |
855 | // int |
856 | // S1_addsub_i: int |
857 | // int |
858 | // S2_presdbl_st: int |
859 | // int |
860 | // S2_presdbl_i: int |
861 | // int |
862 | // S3_zero_st: int |
863 | // int |
864 | // S3_zero_i: int |
865 | // int |
866 | // D_z: int |
867 | // int |
868 | // D_print_st: int |
869 | // int |
870 | // D_print_i: int |
871 | // int |
872 | // N_generate: void (void) |
873 | // void (void) |
874 | // S1_addsub: void (void) |
875 | // void (void) |
876 | // S2_presdbl: void (void) |
877 | // void (void) |
878 | // S3_zero: void (void) |
879 | // void (void) |
880 | // D_print: void (void) |
881 | // void (void) |
882 | // eval: void (void) |
883 | // void (void) |
884 | // start_simulation: void (void) |
885 | // void (void) |
886 | // n1: int |
887 | // int |
888 | // n2: int |
889 | // int |
890 | // n3: int |
891 | // int |
892 | // bound: int |
893 | // int |
894 | // i: int |
895 | // int |
896 | // flag: int |
897 | // int |
898 | // |
899 | |
900 | D_print_i = __VERIFIER_nondet_int(); |
901 | D_print_st = __VERIFIER_nondet_int(); |
902 | D_z = __VERIFIER_nondet_int(); |
903 | N_generate_i = __VERIFIER_nondet_int(); |
904 | N_generate_st = __VERIFIER_nondet_int(); |
905 | S1_addsub_i = __VERIFIER_nondet_int(); |
906 | S1_addsub_st = __VERIFIER_nondet_int(); |
907 | S2_presdbl_i = __VERIFIER_nondet_int(); |
908 | S2_presdbl_st = __VERIFIER_nondet_int(); |
909 | S3_zero_i = __VERIFIER_nondet_int(); |
910 | S3_zero_st = __VERIFIER_nondet_int(); |
911 | count = __VERIFIER_nondet_int(); |
912 | main_clk_ev = __VERIFIER_nondet_int(); |
913 | main_clk_neg_edge = __VERIFIER_nondet_int(); |
914 | main_clk_pos_edge = __VERIFIER_nondet_int(); |
915 | main_clk_req_up = __VERIFIER_nondet_int(); |
916 | main_clk_val = __VERIFIER_nondet_int(); |
917 | main_clk_val_t = __VERIFIER_nondet_int(); |
918 | main_dbl_ev = __VERIFIER_nondet_int(); |
919 | main_dbl_req_up = __VERIFIER_nondet_int(); |
920 | main_dbl_val = __VERIFIER_nondet_int(); |
921 | main_dbl_val_t = __VERIFIER_nondet_int(); |
922 | main_diff_ev = __VERIFIER_nondet_int(); |
923 | main_diff_req_up = __VERIFIER_nondet_int(); |
924 | main_diff_val = __VERIFIER_nondet_int(); |
925 | main_diff_val_t = __VERIFIER_nondet_int(); |
926 | main_in1_ev = __VERIFIER_nondet_int(); |
927 | main_in1_req_up = __VERIFIER_nondet_int(); |
928 | main_in1_val = __VERIFIER_nondet_int(); |
929 | main_in1_val_t = __VERIFIER_nondet_int(); |
930 | main_in2_ev = __VERIFIER_nondet_int(); |
931 | main_in2_req_up = __VERIFIER_nondet_int(); |
932 | main_in2_val = __VERIFIER_nondet_int(); |
933 | main_in2_val_t = __VERIFIER_nondet_int(); |
934 | main_pres_ev = __VERIFIER_nondet_int(); |
935 | main_pres_req_up = __VERIFIER_nondet_int(); |
936 | main_pres_val = __VERIFIER_nondet_int(); |
937 | main_pres_val_t = __VERIFIER_nondet_int(); |
938 | main_sum_ev = __VERIFIER_nondet_int(); |
939 | main_sum_req_up = __VERIFIER_nondet_int(); |
940 | main_sum_val = __VERIFIER_nondet_int(); |
941 | main_sum_val_t = __VERIFIER_nondet_int(); |
942 | main_zero_ev = __VERIFIER_nondet_int(); |
943 | main_zero_req_up = __VERIFIER_nondet_int(); |
944 | main_zero_val = __VERIFIER_nondet_int(); |
945 | main_zero_val_t = __VERIFIER_nondet_int(); |
946 | res = __VERIFIER_nondet_int(); |
947 | |
948 | |
949 | |
950 | { |
951 | int n1 = 3; |
952 | int n2 = 5; |
953 | int n3 = 7; |
954 | res = 0; |
955 | auto int bound; |
956 | bound = __VERIFIER_nondet_int(); |
957 | __VERIFIER_assume(bound >= 1); |
958 | { |
959 | { |
960 | count = 0; |
961 | main_in1_ev = 2; |
962 | main_in1_req_up = 0; |
963 | main_in2_ev = 2; |
964 | main_in2_req_up = 0; |
965 | main_diff_ev = 2; |
966 | main_diff_req_up = 0; |
967 | main_sum_ev = 2; |
968 | main_sum_req_up = 0; |
969 | main_pres_ev = 2; |
970 | main_pres_req_up = 0; |
971 | main_dbl_ev = 2; |
972 | main_dbl_req_up = 0; |
973 | main_zero_ev = 2; |
974 | main_zero_req_up = 0; |
975 | main_clk_val = 0; |
976 | main_clk_ev = 2; |
977 | main_clk_req_up = 0; |
978 | main_clk_pos_edge = 2; |
979 | main_clk_neg_edge = 2; |
980 | count = 0; |
981 | N_generate_i = 0; |
982 | S1_addsub_i = 0; |
983 | S2_presdbl_i = 0; |
984 | S3_zero_i = 0; |
985 | D_print_i = 0; |
986 | start_simulation(); |
987 | } |
988 | { |
989 | int i = 0; |
990 | while (1) { |
991 | if (i < bound) { |
992 | } |
993 | else { |
994 | break; |
995 | } |
996 | { |
997 | if (i % n1 == 0) { |
998 | if (i % n2 == 0) { |
999 | if (i % n3 == 0) { |
1000 | res = i; |
1001 | } |
1002 | else { |
1003 | } |
1004 | } |
1005 | else { |
1006 | } |
1007 | } |
1008 | else { |
1009 | } |
1010 | i ++; |
1011 | int flag = res; |
1012 | while_2_continue: ; |
1013 | { |
1014 | main_clk_val_t = 1; |
1015 | main_clk_req_up = 1; |
1016 | start_simulation(); |
1017 | count ++; |
1018 | } |
1019 | |
1020 | if (res % 105 == 0) { |
1021 | ; |
1022 | } else { |
1023 | error(); |
1024 | } |
1025 | |
1026 | if (count == 5) { |
1027 | if (! (D_z == 0)) { |
1028 | error(); |
1029 | } |
1030 | else { |
1031 | } |
1032 | count = 0; |
1033 | } |
1034 | else { |
1035 | } |
1036 | { |
1037 | main_clk_val_t = 0; |
1038 | main_clk_req_up = 1; |
1039 | start_simulation(); |
1040 | |
1041 | } |
1042 | } |
1043 | } |
1044 | } |
1045 | } |
1046 | return; |
1047 | }} |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2023-06-28 | 04:16:58:978 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2023-06-28 | 04:16:58:996 | INFO | ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2023-06-28 | 04:16:59:051 | INFO | CPAchecker.run | CPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started |
| 2023-06-28 | 04:16:59:071 | INFO | CPAchecker.parse | Parsing CFA from file(s) "no_context/combo1.c" |
| 2023-06-28 | 04:17:00:114 | INFO | CoreComponentsFactory.createAlgorithm | Using heuristics to select analysis |
| 2023-06-28 | 04:17:00:125 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.callstack.unsupportedFunctions termination.violation.witness cpa.predicate.memoryAllocationsAlwaysSucceed cpa.arg.compressWitness cpa.callstack.skipFunctionPointerRecursion cpa.composite.aggregateBasicBlocks counterexample.export.graphml counterexample.export.compressWitness cpa.arg.proofWitness |
| 2023-06-28 | 04:17:00:126 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2023-06-28 | 04:17:00:130 | INFO | SelectionAlgorithm.chooseConfig | Performing heuristic ... |
| 2023-06-28 | 04:17:00:135 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2023-06-28 | 04:17:00:149 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2023-06-28 | 04:17:00:155 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ... |
| 2023-06-28 | 04:17:00:160 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'. |
| 2023-06-28 | 04:17:00:161 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'. |
| 2023-06-28 | 04:17:00:161 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'. |
| 2023-06-28 | 04:17:00:163 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 140s |
| 2023-06-28 | 04:17:00:464 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Starting analysis 1 ... |
| 2023-06-28 | 04:19:07:182 | WARNING | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ShutdownNotifier.shutdownIfNecessary | Warning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.) |
| 2023-06-28 | 04:19:07:372 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | RestartAlgorithm switches to the next configuration... |
| 2023-06-28 | 04:19:07:372 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Loading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ... |
| 2023-06-28 | 04:19:07:375 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'. |
| 2023-06-28 | 04:19:07:375 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'. |
| 2023-06-28 | 04:19:07:376 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'. |
| 2023-06-28 | 04:19:07:376 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 60s |
| 2023-06-28 | 04:19:07:429 | INFO | Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run | Starting analysis 2 ... |
| 2023-06-28 | 04:19:07:522 | INFO | CPAchecker.runAlgorithm | Stopping analysis ... |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Selection Algorithm statistics | ||
| Size of preliminary analysis reached set | 0 | |
| Used algorithm property | /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties | |
| Program containing only relevant bools | 0 | |
| Relevant boolean vars / relevant vars ratio | 0.0685 | |
| Requires alias handling | 0 | |
| Requires loop handling | 1 | |
| Has a single loop | 0 | |
| Requires composite-type handling | 0 | |
| Requires array handling | 0 | |
| Requires float handling | 0 | |
| Requires recursion handling | 0 | |
| Relevant addressed vars / relevant vars ratio | 0.0000 | |
| Program containing external functions | true | |
| Number of all righthand side functions | 9 | |
| Restart Algorithm statistics | ||
| Number of algorithms provided | 7 | |
| Number of algorithms used | 2 | |
| Total time for algorithm 2 | 0.150s | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 0.00 | sum: 0, count: 1449, min: 0, max: 0 |
| Number of global variables per state | 0.00 | sum: 0, count: 1449, min: 0, max: 0 |
| Number of assumptions | 670 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 1782 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.004s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| AutomatonAnalysis (SVCOMP) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.000s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 1.00 | sum: 2120, count: 2120, min: 1, max: 1 [1 x 2120] |
| Number of states with assumption transitions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 1449 | |
| Max size of waitlist | 22 | |
| Average size of waitlist | 12 | |
| Number of computed successors | 1782 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 334 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 0.082s | Max: 0.082s |
| Time for choose from waitlist | 0.017s | |
| Time for precision adjustment | 0.011s | |
| Time for transfer relation | 0.024s | |
| Time for stop operator | 0.003s | |
| Time for adding to reached set | 0.023s | |
| ValueAnalysisRefiner statistics | ||
| Number of refinements | 0 | |
| Number of targets found | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Time for completing refinement | 0.000s | |
| Number of root relocations | 0 | |
| Number of similar, repeated refinements | 0 | |
| Number of unique precision increments | 0 | |
| PathExtractor statistics | ||
| Total number of targets found | 0 | |
| ValueAnalysisPathInterpolator statistics | ||
| Time for interpolation | 0.000s | |
| Number of interpolations | 0 | |
| Number of interpolation queries | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Size of interpolant | 0.00 | sum: 0, count: 0, min: 0, max: 0 |
| Number of sliced prefixes | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Extracting infeasible sliced prefixes | 0.000s | |
| Selecting infeasible sliced prefixes | 0.000s | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 0 | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 1449 | |
| Max size of waitlist | 22 | |
| Average size of waitlist | 12 | |
| Number of computed successors | 1782 | |
| Max successors for one state | 2 | |
| Number of times merged | 0 | |
| Number of times stopped | 334 | |
| Number of times breaked | 0 | |
| Total time for CPA algorithm | 0.082s | Max: 0.082s |
| Time for choose from waitlist | 0.017s | |
| Time for precision adjustment | 0.011s | |
| Time for transfer relation | 0.024s | |
| Time for stop operator | 0.003s | |
| Time for adding to reached set | 0.023s | |
| ValueAnalysisRefiner statistics | ||
| Number of refinements | 0 | |
| Number of targets found | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Time for completing refinement | 0.000s | |
| Number of root relocations | 0 | |
| Number of similar, repeated refinements | 0 | |
| Number of unique precision increments | 0 | |
| PathExtractor statistics | ||
| Total number of targets found | 0 | |
| ValueAnalysisPathInterpolator statistics | ||
| Time for interpolation | 0.000s | |
| Number of interpolations | 0 | |
| Number of interpolation queries | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Size of interpolant | 0.00 | sum: 0, count: 0, min: 0, max: 0 |
| Number of sliced prefixes | 0 | count: 0, min: 0, max: 0, avg: 0.00 |
| Extracting infeasible sliced prefixes | 0.000s | |
| Selecting infeasible sliced prefixes | 0.000s | |
| CEGAR algorithm statistics | ||
| Number of CEGAR refinements | 0 | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 455 | |
| Total lines | 455 | |
| Line coverage | 1.000 | |
| Visited conditions | 234 | |
| Total conditions | 234 | |
| Condition coverage | 1.000 | |
| CPAchecker general statistics | ||
| Number of program locations | 732 | |
| Number of CFA edges (per node) | 861 | count: 732, min: 0, max: 3, avg: 1.18 |
| Number of relevant variables | 73 | |
| Number of functions | 9 | |
| Number of loops (and loop nodes) | 3 | sum: 294, min: 40, max: 196, avg: 98.00 |
| Size of reached set | 1449 | |
| Number of reached locations | 514 | 70% |
| Avg states per location | 2 | |
| Max states per location | 3 | at node N7 |
| Number of reached functions | 9 | 100% |
| Number of target states | 0 | |
| Time for analysis setup | 1.055s | |
| Time for loading CPAs | 0.179s | |
| Time for loading parser | 0.156s | |
| Time for CFA construction | 0.693s | |
| Time for parsing file(s) | 0.262s | |
| Time for AST to CFA | 0.167s | |
| Time for CFA sanity check | 0.048s | |
| Time for post-processing | 0.152s | |
| Time for CFA export | 0.846s | |
| Time for function pointers resolving | 0.005s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.090s | |
| Time for collecting variables | 0.033s | |
| Time for solving dependencies | 0.001s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.051s | |
| Time for exporting data | 0.005s | |
| Time for Analysis | 127.396s | |
| CPU time for analysis | 141.440s | |
| Time for analyzing result | 0.001s | |
| Total time for CPAchecker | 128.452s | |
| Total CPU time for CPAchecker | 144.560s | |
| Time for statistics | 0.051s | |
| Time for Garbage Collector | 0.936s | in 55 runs |
| Garbage Collector(s) used | G1 Old Generation, G1 Young Generation | |
| Used heap memory | 475MB ( 453 MiB) max; 230MB ( 219 MiB) avg; 481MB ( 459 MiB) peak | |
| Used non-heap memory | 53MB ( 50 MiB) max; 50MB ( 48 MiB) avg; 53MB ( 51 MiB) peak | |
| Used in G1 Old Gen pool | 94MB ( 90 MiB) max; 61MB ( 58 MiB) avg; 94MB ( 90 MiB) peak | |
| Allocated heap memory | 638MB ( 609 MiB) max; 544MB ( 519 MiB) avg | |
| Allocated non-heap memory | 56MB ( 53 MiB) max; 53MB ( 51 MiB) avg | |
| Total process virtual memory | 12292MB ( 11723 MiB) max; 12284MB ( 11715 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.entryFunction | main |
| 2 | analysis.name | svcomp23 |
| 3 | analysis.programNames | no_context/combo1.c |
| 4 | analysis.selectAnalysisHeuristically | true |
| 5 | analysis.summaryEdges | true |
| 6 | cfa.simplifyCfa | false |
| 7 | cfa.useCFACloningForMultiThreadedPrograms | true |
| 8 | counterexample.export.compressWitness | false |
| 9 | counterexample.export.graphml | witness.graphml |
| 10 | cpa.arg.compressWitness | false |
| 11 | cpa.arg.proofWitness | witness.graphml |
| 12 | cpa.callstack.skipFunctionPointerRecursion | true |
| 13 | cpa.callstack.unsupportedFunctions | pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow |
| 14 | cpa.composite.aggregateBasicBlocks | false |
| 15 | cpa.predicate.memoryAllocationsAlwaysSucceed | true |
| 16 | datarace.config | svcomp23--datarace.properties |
| 17 | heuristicSelection.addressedRatio | 0.0 |
| 18 | heuristicSelection.complexLoopConfig | components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties |
| 19 | heuristicSelection.loopConfig | components/svcomp23--multipleLoopsConfig.properties |
| 20 | heuristicSelection.loopFreeConfig | components/svcomp23--configselection-restart-bmc-fallbacks.properties |
| 21 | heuristicSelection.singleLoopConfig | components/svcomp23--singleLoopConfig.properties |
| 22 | language | C |
| 23 | limits.time.cpu | 900s |
| 24 | limits.time.cpu::required | 900 |
| 25 | log.level | INFO |
| 26 | memorycleanup.config | svcomp23--memorycleanup.properties |
| 27 | memorysafety.config | svcomp23--memorysafety.properties |
| 28 | overflow.config | svcomp23--overflow.properties |
| 29 | parser.usePreprocessor | true |
| 30 | specification | /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp |
| 31 | statistics.print | true |
| 32 | termination.config | svcomp23--termination.properties |
| 33 | termination.violation.witness | witness.graphml |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}